An interpretation $I$ is a pair $(D,I)$ where:

• $D$ is any set of objects, called domain
• $I$ is a mapping called the interpretation mapping, from the (non logical) symbols to elements and relations over $D$

Given a formula $G$ and an interpretation $I$, if $G$ is true under $I$, we say that $I$ is a model for $G$. 可以记作 $I\models G$

• no matter how we will choose an interpretation, G is always true: G is a valid formula, or a tautology (⊨ G)
• no matter how we will choose an interpretation, G is always false: G is an inconsistent formula
• mind: invalid is different from inconsistent.
• More frequently, there will be formulas G that are invalid, bur are satisfiable (i.e., consistent).

logical consequence

Given a set of formulas $F_1,\cdots ,F_n$ and a formula G, G is said to be a logical consequence of $F_1\wedge \cdots \wedge F_n$ iff for any interpretation $I$ in which F${}_1\wedge \cdots \wedge F_n$ is true, G is also true. Syntactically: $F_1\wedge \cdots \wedge F_n\models G$

• Def.: Two formulas F and G are logically equivalent
• F ≡ G iff the truth values of F and G are the sameunder every interpretation of F and G
• F ≡ 𝑄 iff 𝐹 ⊨ 𝑄 and 𝑄 ⊨ 𝐹

logical equivalence

Refutation and Resolution

Reasoning by refutation

Theorem: Given a set of formulas {𝐹 !, … , 𝐹 # } and a formula G, 𝐹1 ∧ ⋯ ∧ 𝐹n ⊨ 𝐺 if and only if 𝐹 ! ∧ ⋯ ∧ 𝐹 # ∧ ¬𝐺 is inconsistent.

Resolution

Refutation and Resolution together – practical steps

• Transform our knowledge base KB in CNF form: each conjunct will be a clause
• Negate the formula G and add it to the KB
• Apply the resolution principle (to all the clauses) until we reach the inconsistency